00100	PUTPROP('EXPR,'PROCDEF,'STAT);
00200	
00300	EXPR SHOWLINE(LINTXT);
00400	  BEGIN SCALAR NUM,WFF,COM,ASS;
00500		NUM←CAR LINTXT;
00600		WFF←CADR LINTXT;
00700		COM←CADDR LINTXT;
00800		ASS←CADDDR LINTXT;
00900		IF CAR COM = 'ASS THEN ASS←'ASSUMPTION ;
01000		IF CAR COM='USEAX THEN COM←'AXIOM.CDR COM;
01100		IF CAR COM='USESCHM THEN COM←'SCHEMA.CDR COM;
01200		IF CAR COM='USETHM THEN COM←'THEOREM.CDR COM;
01300		TERPRI(); TERPRI();
01400		PRINC NUM;
01500		PRINC ': ;
01600		TABTO 8;
01700		COL←CURCOL();
01800		SHOWEXP WFF;
01900		IF FITSLINE(WFF,COL,0)∧FITSLINE(COM,CURCOL()+4,0)
02000		   THEN PRINC '/  ELSE TABTO 8;
02100		PRINS 'BY ;
02200		COL←CURCOL();
02300		SHOWEXP COM;
02400		IF CAR COM = 'ASS∨NULL ASS THEN RETURN;
02500		IF FITSLINE(COM,COL,0)∧LENGTH ASS+9<CHRCT()
02600		   THEN PRINC '/ ELSE TABTO 8;
02700		PRINS 'ASSUMING ;
02800		PRINS CADDDR LINTXT;
02900		RETURN;
03000	  END;
03100	
03200	END;
03300